$\forall$$P$:(event\_system\{i:l\}$\rightarrow$prop\{i':l\}). es{-}real\{i:l\}(${\it es}$.$P$(${\it es}$)) $\in$ Type\{i''\}